\documentclass[a4paper,12pt]{article}

\usepackage[T2A]{fontenc} 
\usepackage[utf8]{inputenc}
\usepackage[english,russian]{babel}
\usepackage{listings}
\usepackage[dvips]{graphicx}
\usepackage{indentfirst}
\usepackage{color}
\usepackage{hyperref}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{geometry}
\geometry{left=1.5cm}
\geometry{right=1.5cm}
\geometry{top=1cm}
\geometry{bottom=2cm}

\graphicspath{{images/}}

\begin{document}
\sloppy

\lstset{
	basicstyle=\small,
	stringstyle=\ttfamily,
	showstringspaces=false,
	columns=fixed,
	breaklines=true,
	numbers=right,
	numberstyle=\tiny
}

\newtheorem{Def}{Определение}[section]
\newtheorem{Th}{Теорема}
\newtheorem{Lem}[Th]{Лемма}
\newenvironment{Proof}
	{\par\noindent{\bf Доказательство.}}
	{\hfill$\scriptstyle\blacksquare$}
\newenvironment{Solution}
	{\par\noindent{\bf Решение.}}
	{\hfill$\scriptstyle\blacksquare$}


\begin{flushright}
	Кринкин М. Ю. группа 504 (SE)
\end{flushright}

\section{Домашнее задание 2}

\paragraph{Здание 1.} Предложите (и обоснуйте) полиномиальный алгоритм проверки общезначимости КНФ. Изестен ли полиномиальный алгоритм проверки выполнимости КНФ?

\begin{Solution}
КНФ общезначима, если общезначим каждый из ее дизъюнктов. Дизъюнкт общезначим тогда, когда содержит некоторую переменную и ее отрицание, в любом другом случае он не общезнаим, т. к. в последнем случае, интерпритация сопоставляющая каждой перменной входящей в дизъюнкт без отрицания 0, а каждой переменной входящей в дизъюнкт с отрицанием 1 получаем, что дизъюнкт ложен.

Следовательно, для КНФ задача проверки общезначимости сводится к проверки общезначимости каждого из ее дизъюнктов, которая сводится к проверке вхождения переменной и ее отрицания в дизъюнкт. Если дизюнкт содержит $n$ литералов, то проверка его общезначимости в худшем случае может занять не более $\frac{n\left(n-1\right)}{2}$ попарных сравнений литералов.

Пусть, у нас имеются следующие примитивы:
\begin{itemize}
\item $dis$ - дизюнкт (набор литер с номерами от 1)

\item $len\left(dis\right)$ - количество литералов в дизюнкте

\item $dis\left[i\right]$ - $i$-ый литерал дизъюнкта

\item $var\left(lit\right)$ - переменная литерала

\item $neg\left(lit\right)$ - проверка отрицания (истинно, если $lit$ - отрицание переменной, иначе ложно)

\item $xor$ - исключающее или (двуместная булева функция, возращающая истину, если ее операнды различны, и ложь иначе)
\end{itemize}

тогда алгоритм можно записать следующим образом:
\begin{lstlisting}
function test_dis(dis)
	for i = 1 to len(dis)-1
		for j = i+1 to len(dis)
			if var(dis[i]) == var(dis[j]) then
				if neg(dis[i]) xor neg(dis[j]) then
					return true;
	return false
\end{lstlisting}

Алгоритма проверки выполнимости КНФ за полиномиальное время не известно, вообще, эта задача является NP-полной (SAT) согласно теореме Кука.
\end{Solution}

\paragraph{Задание 2.} Опишите алгоритм построения КНФ пропозициональной формулы, основанный на равносильных преобразованиях формул

\begin{Solution}
Понадобятся следующие тавтологии:
\[
	\begin{split}
		& A \supset B \equiv \neg A \lor B \\
		& A \Leftrightarrow B \equiv \left(A \land B\right) \lor \left(\neg A \land \neg B\right) \\
		& \neg \left(A \lor B\right) \equiv \neg A \land \neg B \\
		& \neg \left(A \land B\right) \equiv \neg A \lor \neg B \\
		& \neg \neg A \equiv A \\
		& A \land \left(B \lor C\right) \equiv A \land B \lor A \land C \\
		& A \lor A \land B \equiv A \\
		& A \land \left(A \lor B\right) \equiv A
	\end{split}
\]

На первом этапе требуется заменить все связки $\supset$ и $\Leftrightarrow$ с помощью тавтологий выше.

На втором этапе требуется заменить знак отрицания относящийся к дизъюнкции или конъюнкции воспользовавшись законаями де Моргана (см. тавтологии выше)

Далее необходимо избавиться от двойного отрицания.

На последнем этапе если необходимо пользуемся татологиями поглощения и дистрибутивности.
\end{Solution}

\paragraph{Задание 3.} Докажите, что штрих Шеффера и стрелка Пирса являются единственными связками такими, что любую булеву функцию можно выразить пропозицинальной формулой, в которой из логических связок входит только одна.

\begin{Solution}
Стрелка Пирса определяется следующей таблицей истинности:
\[
	\begin{matrix}
		a & b & a \downarrow b \\
		0 & 0 & 1 \\
		0 & 1 & 0 \\
		1 & 0 & 0 \\
		1 & 1 & 0
	\end{matrix}
\]
Выразим через стрелку Пирса отрицание, конъюнкцию и дизъюнкцию:
\[
	\begin{split}
		& a \downarrow a = \neg a \\
		& \left(a \downarrow a\right) \downarrow \left(b \downarrow b\right) = a \land b \\
		& \left(a \downarrow b\right) \downarrow \left(a \downarrow b\right) = a \lor b
	\end{split}
\]

Штрих Шеффера определяется следующей таблицей истинности:
\[
	\begin{matrix}
		a & b & a | b \\
		0 & 0 & 1 \\
		0 & 1 & 1 \\
		1 & 0 & 1 \\
		1 & 1 & 0
	\end{matrix}
\]
Выразим через штрих Шеффера отрицание, конъюнкцию и дизъюнкцию:
\[
	\begin{split}
		& a | a = \neg a \\
		& \left(a | a\right) | \left(b | b\right) = a \land b \\
		& \left(a | b\right) | \left(a | b\right) = a \lor b
	\end{split}
\]

Во-первых, отметим, что любая композиция булевых функций сохраняющих единицу (или ноль) будет давать булеву функцию сохраняющую единицу (или ноль). Функций не сохраняющих ни единицу ни ноль только две - штрих Шеффера и стрелка Пирса.
\end{Solution}

\paragraph{Задание 4.} Постройте вывод (в виде последовательности или в виде дерева) формулы $p \supset q \equiv \neg q \supset \neg p$

\begin{Solution}
\[
	\begin{split}
		& ~~~~~~~~~~~~~~~~~~~~~~~~~~\rightarrow p \supset q \equiv \neg q \supset \neg p \\
		& ~~~~~~ p \supset q \rightarrow \neg q \supset \neg p ~~~~~~~~~~~~~~~~~~~~~~ \neg q \supset \neg p \rightarrow p \supset q \\
		& ~~~~~~~~ p \supset q, \neg q \rightarrow \neg p ~~~~~~~~~~~~~~~~~~~~~~~~ \neg q \supset \neg p, p \rightarrow q \\
		& \neg q \rightarrow \neg p, p ~~~~~~ p, q, \neg q \rightarrow \neg p ~~~~~~~~ \neg p, p \rightarrow q, \neg q ~~~~~~ \neg q, \neg p, p \rightarrow q \\
		& p,\neg q \rightarrow p ~~~~~~~~~ p,q,\neg q \rightarrow ~~~~~~~~~~~~~~ p \rightarrow q,\neg q, p ~~~~~~ \neg p, p \rightarrow q \\
		& p \rightarrow q,p ~~~~~~~~~~~ p,q \rightarrow q ~~~~~~~~~~~~~~~~~~ q,p \rightarrow q,p ~~~~~~ p \rightarrow p,q
	\end{split}
\]
\end{Solution}

\paragraph{Задание 5.} Доработайте и обоснуйте следующий способ построения КНФ произвольной пропозициональной формулы $A$: построить дерево поиска вывода секвенции $\rightarrow A$, никакой лист которого не содержит связок; затем по листьям этого дерева записать КНФ формулы $A$. Постройте таким способом КНФ формулы $p | \neg q \supset p \equiv \neg r$.

\begin{Solution}
По полученному дереву поиска вывода КНФ строится следующим образом:
\begin{itemize}
\item Каждый лист дерева вывода не содержащий одну и туже переменную в антицеденте и субцеденте соответствует дизъюнкту КНФ

\item Если переменная оказалась членом субцедента, то в соответствующий дизъюнкт входит сама переменная

\item Если переменная оказалась членом антицедента, то в соответствующий дизъюнкт входит ее отрицание
\end{itemize}

Рассмотрим такое построение КНФ на примере:
\[
	\begin{split}
		& ~~~~~~~~~~~~~~~~~~~~~~~~~~\rightarrow p | \neg q \supset p \equiv \neg r \\
		& ~~~~~~~~~~~~~~~~~~~~~~~~~~~p, \neg q \supset p \equiv \neg r \rightarrow \\
		& ~~~~~~~~p, \neg q \supset p, \neg r \rightarrow ~~~~~~~~~~~~~~~~~~ p \rightarrow \neg q \supset p, \neg r \\
		& p, \neg r \rightarrow \neg q ~~~~~~~ \neg r,\neg q,p \rightarrow ~~~~~~~~~~~ \neg q, p \rightarrow p, \neg r \\
		& p,q \rightarrow r ~~~~~~~~~~~~~~ p \rightarrow r,q ~~~~~~~~~~~~~~~~~ r,p \rightarrow p,q
	\end{split}
\]
Восстановленная по дереву поиска вывода КНФ:
\[
	\left(\neg p \lor \neg q \lor r\right)\land\left(\neg p \lor q \lor r\right)
\]
\end{Solution}

\end{document}
